\begin{tabbing}
$\forall$\=$X$:Type\{j\}, ${\it ds}$:fpf(Id; $x$.Type\{i\}), ${\it da}$:fpf(Knd; $k$.Type\{i\}), $x$:ecl(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it base}$:($k$:Knd$\rightarrow$(decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow\mathbb{B}$)$\rightarrow$$X$), ${\it seq}$,${\it and}$,${\it or}$:(\=ecl(${\it ds}$; ${\it da}$)$\rightarrow$ecl(\=${\it ds}$;\+\+
\\[0ex]${\it da}$)
\-\\[0ex]$\rightarrow$$X$$\rightarrow$$X$$\rightarrow$$X$),
\-\\[0ex]${\it repeat}$:(ecl(${\it ds}$; ${\it da}$)$\rightarrow$$X$$\rightarrow$$X$), ${\it act}$,${\it throw}$:(ecl(${\it ds}$; ${\it da}$)$\rightarrow\mathbb{N}\rightarrow$$X$$\rightarrow$$X$),
\\[0ex]${\it catch}$:(ecl(${\it ds}$; ${\it da}$)$\rightarrow$($\mathbb{N}$ List)$\rightarrow$$X$$\rightarrow$$X$).
\-\\[0ex]ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.${\it base}$($k$,${\it test}$);
\\[0ex]$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it seq}$($a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$);
\\[0ex]$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it and}$($a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$);
\\[0ex]$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it or}$($a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$);
\\[0ex]$a$,${\it rec}_{1}$.${\it repeat}$($a$,${\it rec}_{1}$);
\\[0ex]$a$,$n$,${\it rec}_{1}$.${\it act}$($a$,$n$,${\it rec}_{1}$);
\\[0ex]$a$,$n$,${\it rec}_{1}$.${\it throw}$($a$,$n$,${\it rec}_{1}$);
\\[0ex]$a$,$l$,${\it rec}_{1}$.${\it catch}$($a$,$l$,${\it rec}_{1}$))
\-\\[0ex]$\in$ $X$
\end{tabbing}